Lean 4 マクロ

Lean 4からは、SchemeなどのLisp系列で実装されている衛生的マクロが使えるようになっている

これは対話的定理証明支援系(ITP)で初めて衛生的マクロが実装されたとのこと

Lean 3以前はその他のAgda、Coqなどの証明支援系言語と同じように衛生的ではなく、グローバルに定義していた変数名がマクロ展開時の変数名とバッティングするといったことが起こっていた

マクロ関連のドキュメント

syntaxコマンドで構文定義をして、macro_rulesコマンドでマクロの展開・変換の定義をする

macro_rules内で\`(バッククォート)を使い、変数の評価したりするのを制御する

\`()

準クオート(quasiquotation)

アンクォート(unquote)([Sebastian2020]中ではanti-quotation)

$に続く引数を評価する

マクロの例

code:lean

/- パーサーの定義 -/

syntax (priority := high) "{" term,+ "}" : term

/- 二つのマクロ展開/構文変換を定義する -/

macro_rules

| ({$x}) => (Set.singleton $x)

| ({$x, $xs:term,*}) => (Set.insert $x {$xs,*})

Macro Expander(マクロ展開器)・Elaborator

参考

メモ

調査用